Modern architectures often use relaxed memory models in which memory operations may be reordered and executed non-atomically. While these models allow improved hardware performance, they pose an additional burden on the programmer, who is forced to reason about non-sequentially consistent program executions. To allow programmer control over these relaxed executions, processors provide special memory fence instructions.
As multi-core processors become increasingly dominant, highly concurrent algorithms emerge as critical components of many existing systems. Highly-concurrent algorithms are often hard to get right and often rely on subtle ordering of events, an ordering that may be violated under relaxed memory models.
Finding a correct and efficient placement of memory fences for a concurrent program is a challenging task. Using too many fences (over-fencing) hinders performance, while using too few fences (under-fencing) permits executions that violate correctness.
Even for finite-state programs, fence verification under relaxed memory models is a hard problem. Given a finite state program and a safety specification, verifying that the program satisfies the specification under a sufficiently relaxed memory model (such as a SPARC RMO memory model. See, e.g., SPARC International, Inc., “C. The SPARC Architecture Manual,” (Ver. 9), Prentice-Hall, Inc., 1994) is undecidable. For somewhat stronger memory models (such as SPARC “Total Store Order” (TSO) and “Partial Store Order” (PSO)), the problem is decidable but has non-primitive recursive complexity.
Relaxed memory models allow two basic relaxations of sequential consistency: memory operations may be reordered with respect to each other, and stores may be executed non-atomically across processors. Some relaxations can be naturally modeled using store buffers, emulating the actual hardware implementation.
The basic hurdle for automatic verification using those models is that store buffers can grow without a bound, even for programs that are otherwise finite state. To enable automatic program verification on relaxed memory models, a need exists for techniques for automatic verification and inference of memory fences in concurrent programs that can bound these store buffers.
While a number of techniques have been proposed or suggested for automatic verification and inference of memory fences in concurrent programs, they suffer from a number of limitations, which if overcome, could further improve the reliability of the verification and inference of memory fences. For example, a number of existing approaches employ either under-approximations such as bounded checking and testing, or side-step the problem by focusing on a restricted class of programs. For example, V. A. Saraswat et al., “A Theory of Memory Models,” PPoPP, ACM, 161-172 (2007) considers data-race free programs, and S. Owens, “Reasoning About the Implementation of Concurrency Abstractions on x86-TSO,” ECOOP (2010) focuses on programs free from a particular type of data races.